; COMMAND-LINE: --finite-model-find -q
(set-logic HO_ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun |"An Apple"| () $$unsorted)
(declare-fun |"A _"Microsoft __ escape_""| () $$unsorted)
(assert (not (= |"An Apple"| |"A _"Microsoft __ escape_""|)))
(declare-fun tptp.a () $$unsorted)
(declare-fun tptp.b () $$unsorted)
(declare-fun tptp.f ($$unsorted) $$unsorted)
(declare-fun tptp.g ($$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.h ($$unsorted $$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.p ($$unsorted) Bool)
(declare-fun tptp.q ($$unsorted $$unsorted) Bool)
(assert (forall ((Z $$unsorted)) (ite (exists ((X $$unsorted)) (tptp.p X)) (forall ((X $$unsorted)) (tptp.q X X)) (tptp.q Z (ite (forall ((X $$unsorted)) (tptp.p X)) (tptp.f tptp.a) (tptp.f Z))))))
(assert (forall ((X $$unsorted)) (and (@ (@ (lambda ((Y1 $$unsorted) (Y2 $$unsorted)) (tptp.p Y1)) (@ (lambda ((Z1 $$unsorted)) (tptp.g Z1 tptp.b)) tptp.a)) X) (tptp.p (ite (@ (@ (lambda ((Y3 $$unsorted) (Y4 $$unsorted)) (ite (= Y3 Y4) (@ (@ (lambda ((Y1 $$unsorted) (Y2 $$unsorted)) (tptp.p Y1)) tptp.a) tptp.a) (@ (@ (lambda ((Y1 $$unsorted) (Y2 $$unsorted)) (tptp.p Y1)) Y3) Y4))) tptp.b) tptp.b) (tptp.f tptp.a) (tptp.f X))))))
(assert (forall ((X $$unsorted)) (let ((_let_1 (tptp.p X))) (not (and (not (or _let_1 (not (tptp.q X tptp.a)))) _let_1)))))
(assert (forall ((X $$unsorted)) (= (tptp.f tptp.a) (tptp.f X))))
(assert (tptp.p tptp.a))
(assert (tptp.p tptp.a))
(assert (tptp.p tptp.a))


(declare-fun tptp.ia1 () Bool)
(declare-fun tptp.ia2 () Bool)
(declare-fun tptp.ia3 () Bool)
(assert tptp.ia1)
(assert tptp.ia2)
(assert tptp.ia3)
(assert (forall ((X $$unsorted)) (tptp.p X)))
(assert (forall ((X $$unsorted)) (tptp.p X)))
(assert (forall ((X $$unsorted)) (tptp.p X)))
(assert (forall ((X $$unsorted)) (tptp.p X)))
(assert (forall ((X $$unsorted)) (tptp.p X)))
(assert (tptp.p tptp.a))
(assert (tptp.p tptp.a))
(assert (forall ((X $$unsorted)) (tptp.p X)))
(assert (distinct |"A _"Microsoft __ escape_""| |"An Apple"|))
(set-info :filename SYN000_2)
(check-sat)
